$\forall$$u$,$v$,$R$:top. sqequal(Rall(cons($u$; $v$); $x$.$R$($x$)); Rplus($R$($u$); Rall($v$; $x$.$R$($x$))))